Nuprl Definition : int_seg
13,42
postcript
pdf
{
i
..
j
} == {
k
:
|
i
k
<
j
}
latex
Up
int
1
,
int
1
Wellformedness Lemmas
int
seg
wf
,
int
seg
wf
Definitions
{
x
:
A
|
B
(
x
)}
,
,
i
j
<
k
FDL editor aliases
int_seg
origin
} == {k:
| i 
k < j} } == {k:| i k < j} j < k